;<lemma>
; <title>SSF_pilot.1</title>
; <origin>SSF_pilot | TCTM_Ref1 | INITIALISATION/inv4/INV</origin>
(benchmark SSF_pilot_1
; <theories>
;   <theory name="linear_arith"/>
; </theories>
  :logic QF_LIA
;  <typenv>
;    <variable name="x" type="INTEGER"/>
;  </typenv>
  :extrafuns ((x Int))
  :extramacros (
		 (Nat (lambda (?i Int) . (<= 0 ?i)))

		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 )
; <hypothesis>x : NATURAL</hypothesis>
  :assumption (in x Nat)
; <goal>x-1+1 = x</goal>
  :formula
  (not
      (= (+ (- x 1) 1) x)
    )
)
;</lemma>
